x, y:Atom. (x =a y = ff  )  ((x = y)) 

latex

Up	sqequal 1, sqequal 1
Definitions	, t  T, P  Q, x:A. B(x), P & Q, P  Q
Lemmas	bfalse wf, eq atom wf, bool wf, assert of eq atom, not functionality wrt iff, assert of bnot, eqff to assert, iff transitivity, not wf, bnot wf, assert wf